perm filename T7[1,JRA] blob sn#005896 filedate 1972-08-21 generic text, type T, neo UTF8
00100	LE(X1 X2) ↔ R(D(X1 X2)O) ;
00200	LE(D(X1 X2) X1);
00300	LE( D(D(X1 X3) D(X2 X3))  D(D(X1 X2) X3) );
00400	LE(O X1);
00500	R(X1 X1);
00600	(LE(X1 X2) ∧ LE(X2 X1)) → R(X1 X2);
00700	  ;
00800	
00900	 R(D(X1 X1) O); 
01000	∀(X1 X2 X3)( LE( X1  X2) ∧ LE( X2 X3)) → LE( X1  X3);
01100	∀(X1)R(D(X1 O) X1) ; ;
01200	∀(X1 X2 X3)(LE(X1 X2) → LE(D(X3 X2) D(X3 X1)));;
01250	
01300	
01500	
01600	
01700